/* Bogor: An Extensible and Highly-Modular Model Checking Framework
 * Copyright (c) 2002-2005 Kansas State University
 *
 * This software is licensed using the SAnToS Laboratory Open Academic License.
 * You should have received a copy of the License in the top directory of this
 * software distribution package. If not, then write to
 * SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506, USA.
 *
 * The SAnToS Laboratory homepage is located at http://www.cis.ksu.edu/santos.
 * The Bogor homepage is located at http://bogor.projects.cis.ksu.edu.
 */
package edu.ksu.cis.projects.bogor.module;

import static edu.ksu.cis.projects.bogor.ast.BinaryOp.AND;
import static edu.ksu.cis.projects.bogor.ast.BinaryOp.IMPLIES;
import static edu.ksu.cis.projects.bogor.ast.BinaryOp.OR;

import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Properties;
import java.util.Set;
import java.util.logging.Level;
import java.util.logging.Logger;

import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.LoggingConstants;
import edu.ksu.cis.projects.bogor.ast.ApplyExp;
import edu.ksu.cis.projects.bogor.ast.ArrayAccessExp;
import edu.ksu.cis.projects.bogor.ast.BinaryExp;
import edu.ksu.cis.projects.bogor.ast.BinaryOp;
import edu.ksu.cis.projects.bogor.ast.BooleanLiteral;
import edu.ksu.cis.projects.bogor.ast.CastExp;
import edu.ksu.cis.projects.bogor.ast.ConditionalExp;
import edu.ksu.cis.projects.bogor.ast.DoubleLiteral;
import edu.ksu.cis.projects.bogor.ast.Exp;
import edu.ksu.cis.projects.bogor.ast.ExpExtension;
import edu.ksu.cis.projects.bogor.ast.ExtExp;
import edu.ksu.cis.projects.bogor.ast.FieldAccessExp;
import edu.ksu.cis.projects.bogor.ast.FloatLiteral;
import edu.ksu.cis.projects.bogor.ast.Fun;
import edu.ksu.cis.projects.bogor.ast.IdExp;
import edu.ksu.cis.projects.bogor.ast.InstanceofExp;
import edu.ksu.cis.projects.bogor.ast.IntLiteral;
import edu.ksu.cis.projects.bogor.ast.KindofExp;
import edu.ksu.cis.projects.bogor.ast.LetExp;
import edu.ksu.cis.projects.bogor.ast.Literal;
import edu.ksu.cis.projects.bogor.ast.LiteralExp;
import edu.ksu.cis.projects.bogor.ast.LockTestExp;
import edu.ksu.cis.projects.bogor.ast.LockTestOp;
import edu.ksu.cis.projects.bogor.ast.LongLiteral;
import edu.ksu.cis.projects.bogor.ast.NewArrayExp;
import edu.ksu.cis.projects.bogor.ast.NewLockExp;
import edu.ksu.cis.projects.bogor.ast.NewRecordExp;
import edu.ksu.cis.projects.bogor.ast.Node;
import edu.ksu.cis.projects.bogor.ast.NullLiteral;
import edu.ksu.cis.projects.bogor.ast.ParenExp;
import edu.ksu.cis.projects.bogor.ast.StringLiteral;
import edu.ksu.cis.projects.bogor.ast.ThreadTestExp;
import edu.ksu.cis.projects.bogor.ast.UnaryExp;
import edu.ksu.cis.projects.bogor.ast.UnaryOp;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.config.Domain;
import edu.ksu.cis.projects.bogor.module.config.ISelfDescribingModule;
import edu.ksu.cis.projects.bogor.module.config.OptionScope;
import edu.ksu.cis.projects.bogor.module.state.IState;
import edu.ksu.cis.projects.bogor.module.throwable.ArithmeticBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BogorException;
import edu.ksu.cis.projects.bogor.module.throwable.CastBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExtFailedBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IndexOutOfBoundsBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.NullPointerBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.RangeBogorException;
import edu.ksu.cis.projects.bogor.module.value.IArrayValue;
import edu.ksu.cis.projects.bogor.module.value.IDoubleValue;
import edu.ksu.cis.projects.bogor.module.value.IFloatValue;
import edu.ksu.cis.projects.bogor.module.value.IIntValue;
import edu.ksu.cis.projects.bogor.module.value.ILockValue;
import edu.ksu.cis.projects.bogor.module.value.ILongValue;
import edu.ksu.cis.projects.bogor.module.value.INonPrimitiveValue;
import edu.ksu.cis.projects.bogor.module.value.INullValue;
import edu.ksu.cis.projects.bogor.module.value.IPrimitiveExtValue;
import edu.ksu.cis.projects.bogor.module.value.IRecordValue;
import edu.ksu.cis.projects.bogor.module.value.IStringValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.symboltable.ExtSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.FSMSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.type.ArrayType;
import edu.ksu.cis.projects.bogor.type.DoubleType;
import edu.ksu.cis.projects.bogor.type.FloatType;
import edu.ksu.cis.projects.bogor.type.IntRangeType;
import edu.ksu.cis.projects.bogor.type.IntType;
import edu.ksu.cis.projects.bogor.type.LongRangeType;
import edu.ksu.cis.projects.bogor.type.LongType;
import edu.ksu.cis.projects.bogor.type.NonPrimitiveType;
import edu.ksu.cis.projects.bogor.type.NullType;
import edu.ksu.cis.projects.bogor.type.RecordType;
import edu.ksu.cis.projects.bogor.type.Type;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Pair;
import edu.ksu.cis.projects.bogor.util.Triple;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.trove.custom.IntSet;

/**
 * @author <a href="mailto:robby@cis.ksu.edu">Robby </a>
 * @author <a href="mailto:matt@cis.ksu.edu">Matt Hoosier </a>
 * @version CVS $Revision: 1.36 $ $Date: 2005/11/16 23:24:42 $
 */
public class DefaultExpEvaluator
    implements IExpEvaluator, ISelfDescribingModule
{
    // ~ Instance variables
    // .....................................................

    protected IExpEvaluator ee;

    protected ISchedulingStrategyContext ssc;

    protected ISchedulingStrategyInfo ssi;

    protected ISchedulingStrategist ss;

    protected IValueFactory vf;

    protected SymbolTable symbolTable;

    protected Map<ExtSymbolTable, IModule> extTable;

    protected Type booleanType;

    protected Type[] arrayFieldTypes;

    protected IntSet readGlobals;

    protected Set<IValue> readValues;

    /**
     * @uml.property name="readFieldsTable"
     */
    protected Map<IRecordValue, IntSet> readFieldsTable;

    protected HashMap<String, IValue> bindingMap = new HashMap<String, IValue>();

    // ~ Methods
    // ................................................................

    public String getCopyrightNotice()
    {
        return null;
    }

    public IMessageStore setOptions(String key, Properties configuration)
    {
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

        for (Object o : configuration.keySet())
        {
            String optionId = (String) o;

            if (optionId.startsWith(key) && !optionId.equals(key))
            {
                warnings.add(FileMessage.buildMessage(
                    optionId,
                    ConfigurationMessages.UNKNOWN_OPTION,
                    new String[]
                        {
                            optionId
                        }));
            }
        }

        return warnings.isEmpty()
            ? new DefaultMessageStore()
            : new DefaultMessageStore(new ArrayList<FileMessage>(0), warnings);
    }

    /**
     * @uml.property name="readFieldsTable"
     */
    public void setReadFieldsTable(Map<IRecordValue, IntSet> readFieldsTable)
    {
        this.readFieldsTable = readFieldsTable;
    }

    public void setReadGlobalSet(IntSet readGlobals)
    {
        this.readGlobals = readGlobals;
    }

    public void setReadValueSet(Set<IValue> readValues)
    {
        this.readValues = readValues;
    }

    public Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo> setSchedulingStrategyContextInfo(
        ISchedulingStrategyContext ssc,
        ISchedulingStrategyInfo ssi)
    {
        assert ((ssc != null) && (ssi != null));

        Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo> result = new Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo>(
            this.ssc,
            this.ssi);

        this.ssc = ssc;
        this.ssi = ssi;

        return result;
    }

    public IMessageStore connect(IBogorConfiguration bc)
    {
        assert (bc != null);
        this.symbolTable = bc.getSymbolTable();
        this.ee = bc.getExpEvaluator();
        this.vf = bc.getValueFactory();
        this.ss = bc.getSchedulingStrategist();
        this.extTable = bc.getExtTable();

        int size = symbolTable.getArrayFieldCount();
        arrayFieldTypes = new Type[size];

        int j = 0;

        for (Iterator<String> i = symbolTable.getArrayFieldNameIterator(); i
            .hasNext(); j++)
        {
            String fieldName = i.next();
            int index = symbolTable.getArrayFieldIndex(fieldName);
            arrayFieldTypes[index] = symbolTable.getArrayFieldType(fieldName);
        }

        booleanType = symbolTable.getTypeFactory().getBooleanType();

        return new DefaultMessageStore();
    }

    public void dispose()
    {
        this.symbolTable = null;
        this.ee = null;
        this.vf = null;
        this.ss = null;
        extTable = null;

        if (arrayFieldTypes != null)
        {
            int size = arrayFieldTypes.length;

            for (int i = 0; i < size; i++)
            {
                arrayFieldTypes[i] = null;
            }

            arrayFieldTypes = null;
        }

        booleanType = null;
    }

    /**
     * <p>
     * Evalute a BIR expression using the given context (current function,
     * thread ID, etc).
     * </p>
     * <p>
     * In general, this method may raise any excpetion documented by another
     * public method on the <tt>IExpEvaluator</tt> interface. Any method
     * defined there is reachable from this entry point. A listing of the
     * exception types which might be raised is given below.
     * </p>
     * 
     * @throws ArithmeticBogorException
     * @throws CastBogorException
     * @throws ExtFailedBogorException
     * @throws IndexOutOfBoundsBogorException
     * @throws NullPointerBogorException
     * @throws RangeBogorException
     */
    public IValue evaluate(
        ISchedulingStrategyContext ssc,
        Exp exp,
        ISchedulingStrategyInfo ssi)
    {
        assert ((ssc != null) && (exp != null) && (ssi != null));

        ISchedulingStrategyContext oldSSC = this.ssc;
        ISchedulingStrategyInfo oldSSI = this.ssi;

        ee.setSchedulingStrategyContextInfo(ssc, ssi);

        IValue result = evaluate(exp);
        ee.unsetSchedulingStrategyContextInfo();

        this.ssc = oldSSC;
        this.ssi = oldSSI;

        return result;
    }

    public IValue evaluateApply(String id, IValue[] args)
    {
        Fun fun = (Fun) symbolTable.getIdentifierDefTable().get(id);

        HashMap<String, IValue> oldBindings = new HashMap<String, IValue>();

        HashSet<String> addedBindingIds = new HashSet<String>();
        int size = args.length;

        for (int i = 0; i < size; i++)
        {
            String paramId = fun.getParam(i).getId();
            IValue arg = args[i];
            IValue oldBinding = bindingMap.get(paramId);

            if (oldBinding != null)
            {
                oldBindings.put(paramId, oldBinding);
            }

            addedBindingIds.add(paramId);
            bindingMap.put(paramId, arg);
        }

        try
        {
            return evaluate(fun.getExp());
        }
        finally
        {
            for (Iterator<String> i = addedBindingIds.iterator(); i.hasNext();)
            {
                bindingMap.remove(i.next());
            }

            bindingMap.putAll(oldBindings);
            addedBindingIds.clear();
            oldBindings.clear();
        }
    }

    /**
     * @throws IndexOutOfBoundsBogorException
     *             if <tt>arrayValue</tt> is not at least
     *             <tt>indexValue + 1</tt> elements long or
     *             <tt>indexValue < 0</tt>
     */
    public IValue evaluateArrayAccess(
        IArrayValue arrayValue,
        IIntValue indexValue)
    {
        assert ((ssc != null) && (ssi != null) && (arrayValue != null) && (indexValue != null));

        if (readValues != null)
        {
            readValues.add(arrayValue);
        }

        int indexVal = indexValue.getInteger();

        if ((indexVal >= 0) && (indexVal < arrayValue.getLength()))
        {
            return arrayValue.getElementValue(indexVal);
        }
        else
        {
            throw new IndexOutOfBoundsBogorException();
        }
    }

    public IValue evaluateBinaryOp(BinaryOp binop, IValue value1, IValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        if (value1 instanceof INonPrimitiveValue
            && value2 instanceof INonPrimitiveValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (INonPrimitiveValue) value1,
                (INonPrimitiveValue) value2);
        }

        if (value1 instanceof IPrimitiveExtValue
            && value2 instanceof IPrimitiveExtValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (IPrimitiveExtValue) value1,
                (IPrimitiveExtValue) value2);
        }
        else if (value1 instanceof IIntValue && value2 instanceof IIntValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (IIntValue) value1,
                (IIntValue) value2);
        }
        else if (value1 instanceof ILongValue && value2 instanceof ILongValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (ILongValue) value1,
                (ILongValue) value2);
        }
        else if (value1 instanceof ILongValue && value2 instanceof IIntValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (ILongValue) value1,
                (IIntValue) value2);
        }
        else if (value1 instanceof IFloatValue && value2 instanceof IFloatValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (IFloatValue) value1,
                (IFloatValue) value2);
        }
        else if (value1 instanceof IDoubleValue
                 && value2 instanceof IDoubleValue)
        {
            return ee.evaluateBinaryOp(
                binop,
                (IDoubleValue) value1,
                (IDoubleValue) value2);
        }
        else
        {
            assert false;

            return null;
        }
    }

    public IValue evaluateBinaryOp(
        BinaryOp binop,
        INonPrimitiveValue value1,
        INonPrimitiveValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        int result = 0;

        switch (binop)
        {
            case EQ:

                if (value1 instanceof IStringValue
                    && value2 instanceof IStringValue)
                {
                    result = ((IStringValue) value1).getString().equals(
                        ((IStringValue) value2).getString()) ? 1 : 0;
                }
                else
                {
                    result = (value1.getReferenceId() == value2
                        .getReferenceId()) ? 1 : 0;
                }

                break;

            case NEQ:

                if (value1 instanceof IStringValue
                    && value2 instanceof IStringValue)
                {
                    result = (!((IStringValue) value1).getString().equals(
                        ((IStringValue) value2).getString())) ? 1 : 0;
                }
                else
                {
                    result = (value1.getReferenceId() != value2
                        .getReferenceId()) ? 1 : 0;
                }

                break;

            default:
                assert false;
        }

        return vf.newIntValue(booleanType, result);
    }

    public IValue evaluateBinaryOp(
        BinaryOp binop,
        IPrimitiveExtValue value1,
        IPrimitiveExtValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        int result = 0;

        switch (binop)
        {
            case EQ:
                result = (value1.equals(value2)) ? 1 : 0;

                break;

            case NEQ:
                result = (!value1.equals(value2)) ? 1 : 0;

                break;

            default:
                assert false;
        }

        return vf.newIntValue(booleanType, result);
    }

    /**
     * @throws ArithmeticBogorException
     *             if division by zero is requested
     */
    public IValue evaluateBinaryOp(
        BinaryOp binop,
        IIntValue value1,
        IIntValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        int result = 0;
        boolean resultIsBoolean;

        int val1 = value1.getInteger();
        int val2 = value2.getInteger();

        switch (binop)
        {
            case ADD:
                result = val1 + val2;
                resultIsBoolean = false;

                break;

            case AND:
                assert ((val1 == 0) || (val1 == 1) || (val2 == 0) || (val2 == 1));
                result = ((val1 + val2) == 2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case DIV:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 / val2;
                resultIsBoolean = false;

                break;

            case EQ:
                result = (val1 == val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case GT:
                result = (val1 > val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case GTE:
                result = (val1 >= val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case IMPLIES:
                assert ((val1 == 0) || (val1 == 1) || (val2 == 0) || (val2 == 1));
                result = ((val1 == 0) || (val2 == 1)) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case LT:
                result = (val1 < val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case LTE:
                result = (val1 <= val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case MOD:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 % val2;
                resultIsBoolean = false;

                break;

            case MUL:
                result = val1 * val2;
                resultIsBoolean = false;

                break;

            case NEQ:
                result = (val1 != val2) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case OR:
                assert ((val1 == 0) || (val1 == 1) || (val2 == 0) || (val2 == 1));
                result = ((val1 + val2) > 0) ? 1 : 0;
                resultIsBoolean = true;

                break;

            case SUB:
                result = val1 - val2;
                resultIsBoolean = false;

                break;

            case BIT_AND:
                result = val1 & val2;
                resultIsBoolean = false;

                break;

            case BIT_OR:
                result = val1 | val2;
                resultIsBoolean = false;

                break;

            case BIT_XOR:
                result = val1 ^ val2;
                resultIsBoolean = false;

                break;

            case SHL:
                result = val1 << val2;
                resultIsBoolean = false;

                break;

            case SHR:
                result = val1 >> val2;
                resultIsBoolean = false;

                break;

            case USHR:
                result = val1 >>> val2;
                resultIsBoolean = false;

                break;

            default:
                resultIsBoolean = false;
                assert false;
        }

        if (resultIsBoolean)
        {
            return vf.newIntValue(booleanType, result);
        }
        else
        {
            return vf.newIntValue(result);
        }
    }

    /**
     * @throws ArithmeticBogorException
     *             if division by zero is requested
     */
    public IValue evaluateBinaryOp(
        BinaryOp binop,
        ILongValue value1,
        ILongValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        long result = 0;
        boolean resultIsBoolean;
        long val1 = value1.getLong();
        long val2 = value2.getLong();

        switch (binop)
        {
            case ADD:
                result = val1 + val2;

                break;

            case DIV:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 / val2;

                break;

            case EQ:
                return vf.newIntValue(booleanType, (val1 == val2) ? 1 : 0);

            case GT:
                return vf.newIntValue(booleanType, (val1 > val2) ? 1 : 0);

            case GTE:
                return vf.newIntValue(booleanType, (val1 >= val2) ? 1 : 0);

            case LT:
                return vf.newIntValue(booleanType, (val1 < val2) ? 1 : 0);

            case LTE:
                return vf.newIntValue(booleanType, (val1 <= val2) ? 1 : 0);

            case MOD:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 % val2;

                break;

            case MUL:
                result = val1 * val2;

                break;

            case NEQ:
                return vf.newIntValue(booleanType, (val1 != val2) ? 1 : 0);

            case SUB:
                result = val1 - val2;

                break;

            case BIT_AND:
                result = val1 & val2;

                break;

            case BIT_OR:
                result = val1 | val2;

                break;

            case BIT_XOR:
                result = val1 ^ val2;

                break;

            case SHL:
                result = val1 << val2;

                break;

            case SHR:
                result = val1 >> val2;

                break;

            case USHR:
                result = val1 >>> val2;

                break;

            default:
                assert false;
        }

        return vf.newLongValue(result);
    }

    /**
     * @throws ArithmeticBogorException
     *             if division by zero is requested
     */
    public IValue evaluateBinaryOp(
        BinaryOp binop,
        ILongValue value1,
        IIntValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        long result = 0;
        long val1 = value1.getLong();
        int val2 = value2.getInteger();

        switch (binop)
        {
            case SHL:
                result = val1 << val2;

                break;

            case SHR:
                result = val1 >> val2;

                break;

            case USHR:
                result = val1 >>> val2;

                break;

            default:
                assert false;
        }

        return vf.newLongValue(result);
    }

    /**
     * @throws ArithmeticBogorException
     *             if division by zero is requested
     */
    public IValue evaluateBinaryOp(
        BinaryOp binop,
        IFloatValue value1,
        IFloatValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        float result = 0;
        float val1 = value1.getFloat();
        float val2 = value2.getFloat();

        switch (binop)
        {
            case ADD:
                result = val1 + val2;

                break;

            case DIV:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 / val2;

                break;

            case EQ:
                return vf.newIntValue(booleanType, (val1 == val2) ? 1 : 0);

            case GT:
                return vf.newIntValue(booleanType, (val1 > val2) ? 1 : 0);

            case GTE:
                return vf.newIntValue(booleanType, (val1 >= val2) ? 1 : 0);

            case LT:
                return vf.newIntValue(booleanType, (val1 < val2) ? 1 : 0);

            case LTE:
                return vf.newIntValue(booleanType, (val1 <= val2) ? 1 : 0);

            case MOD:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 % val2;

                break;

            case MUL:
                result = val1 * val2;

                break;

            case NEQ:
                return vf.newIntValue(booleanType, (val1 != val2) ? 1 : 0);

            case SUB:
                result = val1 - val2;

                break;

            default:
                assert false;
        }

        return vf.newFloatValue(result);
    }

    /**
     * @throws ArithmeticBogorException
     *             if division by zero is requested
     */
    public IValue evaluateBinaryOp(
        BinaryOp binop,
        IDoubleValue value1,
        IDoubleValue value2)
    {
        assert ((ssc != null) && (ssi != null) && (value1 != null) && (value2 != null));

        double result = 0;
        double val1 = value1.getDouble();
        double val2 = value2.getDouble();

        switch (binop)
        {
            case ADD:
                result = val1 + val2;

                break;

            case DIV:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 / val2;

                break;

            case EQ:
                return vf.newIntValue(booleanType, (val1 == val2) ? 1 : 0);

            case GT:
                return vf.newIntValue(booleanType, (val1 > val2) ? 1 : 0);

            case GTE:
                return vf.newIntValue(booleanType, (val1 >= val2) ? 1 : 0);

            case LT:
                return vf.newIntValue(booleanType, (val1 < val2) ? 1 : 0);

            case LTE:
                return vf.newIntValue(booleanType, (val1 <= val2) ? 1 : 0);

            case MOD:

                if (val2 == 0)
                {
                    throw new ArithmeticBogorException();
                }

                result = val1 % val2;

                break;

            case MUL:
                result = val1 * val2;

                break;

            case NEQ:
                return vf.newIntValue(booleanType, (val1 != val2) ? 1 : 0);

            case SUB:
                result = val1 - val2;

                break;

            default:
                assert false;
        }

        return vf.newDoubleValue(result);
    }

    /**
     * @throw BogorCastException if the r-value is not statically
     *        assignment-compatible with the l-value type <tt>castType</tt>
     * @throw RangeBogorException if the r-value type <tt>valueType</tt> is an
     *        integral range (non-wrap) type, the l-value type <tt>castType</tt>
     *        is also a integral range type, and <tt>value</tt>'s numerical
     *        value is outside the bounds of <tt>castType</tt>'s domain
     */
    public IValue evaluateCast(Type castType, Type valueType, IValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        IValue result = null;

        if (castType == valueType)
        {
            result = value;
        }
        else if (castType instanceof IntType && valueType instanceof IntType)
        {
            result = ee.evaluateCast((IntType) castType, (IIntValue) value);
        }
        else if (castType instanceof LongType && valueType instanceof LongType)
        {
            result = ee.evaluateCast((LongType) castType, (ILongValue) value);
        }
        else if (castType instanceof LongType && valueType instanceof IntType)
        {
            result = ee.evaluateCast((LongType) castType, (IIntValue) value);
        }
        else if (castType instanceof IntType && valueType instanceof LongType)
        {
            result = ee.evaluateCast((IntType) castType, (ILongValue) value);
        }
        else if (castType instanceof IntType && valueType instanceof FloatType)
        {
            result = ee.evaluateCast((IntType) castType, (IFloatValue) value);
        }
        else if (castType instanceof IntType && valueType instanceof DoubleType)
        {
            result = ee.evaluateCast((IntType) castType, (IDoubleValue) value);
        }
        else if (castType instanceof LongType && valueType instanceof FloatType)
        {
            result = ee.evaluateCast((LongType) castType, (IFloatValue) value);
        }
        else if (castType instanceof LongType
                 && valueType instanceof DoubleType)
        {
            result = ee.evaluateCast((LongType) castType, (IDoubleValue) value);
        }
        else if (castType instanceof FloatType && valueType instanceof IntType)
        {
            result = ee.evaluateCastFloat((IIntValue) value);
        }
        else if (castType instanceof DoubleType && valueType instanceof IntType)
        {
            result = ee.evaluateCastDouble((IIntValue) value);
        }
        else if (castType instanceof FloatType && valueType instanceof LongType)
        {
            result = ee.evaluateCastFloat((ILongValue) value);
        }
        else if (castType instanceof FloatType
                 && valueType instanceof DoubleType)
        {
            result = ee.evaluateCastFloat((IDoubleValue) value);
        }
        else if (castType instanceof DoubleType
                 && valueType instanceof LongType)
        {
            result = ee.evaluateCastDouble((ILongValue) value);
        }
        else if (castType instanceof DoubleType
                 && valueType instanceof FloatType)
        {
            result = ee.evaluateCastDouble((IFloatValue) value);
        }
        else if (castType instanceof NonPrimitiveType
                 && value instanceof INullValue)
        {
            result = value;
        }
        else if (castType instanceof ArrayType
                 && valueType instanceof ArrayType)
        {
            result = ee.evaluateCast((ArrayType) castType, (IArrayValue) value);
        }
        else if (castType instanceof ArrayType
                 && valueType instanceof RecordType)
        {
            IValue v = ee.evaluateCast(
                (ArrayType) castType,
                (IArrayValue) value);

            if (v.getType() instanceof ArrayType)
            {
                result = ee.evaluateCast(
                    (ArrayType) castType,
                    (IArrayValue) value);
            }
            else
            {
                throw new CastBogorException();
            }
        }
        else if (castType instanceof RecordType
                 && valueType instanceof ArrayType)
        {
            RecordType rt = (RecordType) castType;
            String s = symbolTable.getTopRecordName();

            if (s.equals(rt.getId()))
            {
                result = value;
            }
            else
            {
                throw new CastBogorException();
            }
        }
        else if (castType instanceof RecordType
                 && valueType instanceof RecordType)
        {
            result = ee.evaluateCast(
                (RecordType) castType,
                (IRecordValue) value);
        }
        else if (castType instanceof NonPrimitiveType
                 && valueType instanceof NullType)
        {
            result = value;
        }
        else
        {
            assert false;
        }

        return result;
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the logical value of <tt>value</tt>
     */
    public IIntValue evaluateCast(IntType castType, IIntValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return (IIntValue) checkRange(castType, value);
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the logical value of <tt>value</tt>
     */
    public ILongValue evaluateCast(LongType castType, ILongValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return (ILongValue) checkRange(castType, value);
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the logical value of <tt>value</tt>
     */
    public ILongValue evaluateCast(LongType castType, IIntValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee.evaluateCast(castType, vf.newLongValue(value.getInteger()));
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the logical value of <tt>value</tt>
     */
    public IIntValue evaluateCast(IntType castType, ILongValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee.evaluateCast(castType, vf.newIntValue((int) value.getLong()));
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the <tt>int</tt> coercion of
     *        <tt>value</tt>
     */
    public IIntValue evaluateCast(IntType castType, IFloatValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee
            .evaluateCast(castType, vf.newIntValue((int) value.getFloat()));
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the <tt>int</tt> coercion of
     *        <tt>value</tt>
     */
    public IIntValue evaluateCast(IntType castType, IDoubleValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee.evaluateCast(castType, vf
            .newIntValue((int) value.getDouble()));
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the <tt>long</tt> coercion of
     *        <tt>value</tt>
     */
    public ILongValue evaluateCast(LongType castType, IFloatValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee.evaluateCast(castType, vf.newLongValue((long) value
            .getFloat()));
    }

    /**
     * @throw RangeBogorException if <tt>castType</tt> is a non-wrapped range
     *        type which does not contain the <tt>long</tt> coercion of
     *        <tt>value</tt>
     */
    public ILongValue evaluateCast(LongType castType, IDoubleValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        return ee.evaluateCast(castType, vf.newLongValue((long) value
            .getDouble()));
    }

    /**
     * @throw CastBogorException if the runtime type of <tt>value</tt> is not
     *        a subtype (reflexive) of <tt>castType</tt>
     */
    public IRecordValue evaluateCast(RecordType castType, IRecordValue value)
    {
        assert ((ssc != null) && (ssi != null) && (castType != null)
                && (value != null) && !(value instanceof IArrayValue));

        Type valueType = value.getType();
        String castName = castType.getId();
        String valueName = ((RecordType) valueType).getId();

        if ((castType != valueType)
            && !symbolTable.isSubRecord(valueName, castName))
        {
            throw new CastBogorException();
        }

        return value;
    }

    /**
     * @throw CastBogorException if (1) the rank of <tt>value</tt>'s runtime
     *        type and the rank of <tt>castType</tt> do not match, the base
     *        element types are records and <tt>base-type(value.getType())</tt>
     *        is not a subtype of <tt>base-type(castType)</tt>, or (3) the
     *        base element types are non-equal primitives
     */
    public IArrayValue evaluateCast(ArrayType castType, IArrayValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (castType != null));

        Type valueType = value.getType();
        ArrayType castArrayType = castType;
        ArrayType expArrayType = (ArrayType) valueType;

        if (castArrayType == expArrayType)
        {
            // ok
        }
        else if (castArrayType.getRank() != expArrayType.getRank())
        {
            throw new CastBogorException();
        }
        else if (castArrayType.getBaseType() instanceof RecordType
                 && expArrayType.getBaseType() instanceof RecordType)
        {
            String castBaseName = ((RecordType) castArrayType.getBaseType())
                .getId();
            String expBaseName = ((RecordType) expArrayType.getBaseType())
                .getId();

            if (!symbolTable.isSubRecord(expBaseName, castBaseName))
            {
                throw new CastBogorException();
            }
        }
        else
        {
            throw new CastBogorException();
        }

        return value;
    }

    public IDoubleValue evaluateCastDouble(IIntValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newDoubleValue(value.getInteger());
    }

    public IDoubleValue evaluateCastDouble(ILongValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newDoubleValue(value.getLong());
    }

    public IDoubleValue evaluateCastDouble(IFloatValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newDoubleValue(value.getFloat());
    }

    public IFloatValue evaluateCastFloat(IIntValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newFloatValue(value.getInteger());
    }

    public IFloatValue evaluateCastFloat(ILongValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newFloatValue(value.getLong());
    }

    public IFloatValue evaluateCastFloat(IDoubleValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        return vf.newFloatValue((float) value.getDouble());
    }

    /**
     * @throws ExtFailedBogorException
     *             if the user code raises some exception not rooted at
     *             {@link BogorException}
     * @throws BogorException
     *             if the user code raises some exception inheriting from
     *             {@link BogorException} to signal a malformed BIR model. This
     *             is the exception instance thrown by the user code.
     */
    public IValue evaluateExt(
        String expExtId,
        final Node node,
        final Type[] typeVarArgs,
        final IValue[] args)
    {
        final ExtSymbolTable est = symbolTable.getExpActionExtTable().get(
            expExtId);
        final int size2 = typeVarArgs.length;
        Method m = est.getMethod();
        assert ((est != null) && (typeVarArgs != null) && (m != null));

        IExtArguments extArgs = new IExtArguments()
            {
                public int getExtDesc()
                {
                    return est.getExtDesc();
                }

                public Node getNode()
                {
                    return node;
                }

                public ISchedulingStrategyContext getSchedulingStrategyContext()
                {
                    return ssc;
                }

                public ISchedulingStrategyInfo getSchedulingStrategyInfo()
                {
                    return ssi;
                }

                public int getTypeVariableArgumentCount()
                {
                    return size2;
                }

                public Type getTypeVariableArgument(int index)
                {
                    assert ((index >= 0) && (index < size2));

                    return typeVarArgs[index];
                }

                public int getArgumentCount()
                {
                    return args.length;
                }

                public IValue getArgument(int index)
                {
                    assert ((index >= 0) && (index < args.length));

                    return args[index];
                }

                public void dispose()
                {
                }

                public Type getExpType()
                {
                    return (Type) node.getProperty(Exp.TYPE);
                }

                public ITransformationBacktrackingInfo getContainingTransition()
                {
                    return null;
                }
            };

        try
        {
//        	System.out.println(m.getParameterTypes());
        	IModule obj = extTable.get(est);
//        	System.out.println();
//        	System.out.println(new Object[]
//                {
//                    extArgs
//                });
            return (IValue) m.invoke(extTable.get(est), new Object[]
                {
                    extArgs
                });
        }
        catch (BogorException mce)
        {
            // This case probably isn't reachable, since the reflection
            // subsystem wraps the actual BogorException thrown by client
            // code into an InvocationTargetException (handled below).
            throw mce;
        }
        catch (InvocationTargetException ite)
        {
            // Check to see if the "real" exception is a BogorException thrown
            // explicitly by extension code. If so, bubble it back up the
            // call stack.
            if (ite.getTargetException() instanceof BogorException)
            {
                throw (BogorException) ite.getTargetException();
            }
            else
            {
                Logger.getLogger(LoggingConstants.EXTENSION_LOG_NAME).log(
                    Level.WARNING,
                    "Uncaught throwable in user code",
                    ite);
                throw new ExtFailedBogorException();
            }
        }
        catch (Throwable t)
        {
            Logger.getLogger(LoggingConstants.EXTENSION_LOG_NAME).log(
                Level.WARNING,
                "Uncaught throwable in user code",
                t);
            throw new ExtFailedBogorException();
        }
    }

    public IValue evaluateFieldAccess(IRecordValue value, int fieldIndex)
    {
        assert ((ssc != null) && (ssi != null) && (value != null)
                && (fieldIndex >= 0) && (fieldIndex < value.getFieldCount()));

        if (readValues != null)
        {
            readValues.add(value);
        }

        if (readFieldsTable != null)
        {
            IntSet fieldIndices = readFieldsTable.get(value);

            if (fieldIndices == null)
            {
                fieldIndices = new IntSet();
                readFieldsTable.put(value, fieldIndices);
            }

            fieldIndices.add(fieldIndex);
        }

        return value.getFieldValue(fieldIndex);
    }

    public IIntValue evaluateInstanceof(IValue value, Type instanceofType)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (instanceofType != null));

        if (value instanceof INullValue)
        {
            return vf.newIntValue(0);
        }

        IIntValue result = null;
        Type expType = value.getType();

        if (instanceofType instanceof RecordType
            && expType instanceof RecordType)
        {
            String typeName = ((RecordType) instanceofType).getId();
            String expName = ((RecordType) expType).getId();

            if ((instanceofType == expType)
                || symbolTable.isSubRecord(expName, typeName))
            {
                result = vf.newIntValue(1);
            }
            else
            {
                result = vf.newIntValue(0);
            }
        }
        else if (instanceofType instanceof RecordType
                 && expType instanceof ArrayType)
        {
            result = vf.newIntValue(0);
        }
        else if (instanceofType instanceof ArrayType
                 && expType instanceof RecordType)
        {
            result = vf.newIntValue(0);
        }
        else if (instanceofType instanceof ArrayType
                 && expType instanceof ArrayType)
        {
            if (instanceofType != expType)
            {
                // Check for co-variant compatibility when the base element type
                // is a record
                ArrayType typeArrayType = (ArrayType) instanceofType;
                ArrayType expTypeArrayType = (ArrayType) expType;
                Type typeBaseType = typeArrayType.getBaseType();
                Type expTypeBaseType = expTypeArrayType.getBaseType();

                if (typeBaseType instanceof RecordType
                    && expTypeBaseType instanceof RecordType)
                {
                    String typeName = ((RecordType) typeBaseType).getId();
                    String expName = ((RecordType) expTypeBaseType).getId();

                    if (typeArrayType.getRank() != expTypeArrayType.getRank())
                    {
                        result = vf.newIntValue(0);
                    }
                    else if (typeBaseType != expTypeBaseType
                             && !symbolTable.isSubRecord(expName, typeName))
                    {
                        result = vf.newIntValue(0);
                    }
                    else
                    {
                        result = vf.newIntValue(1);
                    }
                }
                else
                {
                    result = vf.newIntValue(0);
                }
            }
            else
            {
                result = vf.newIntValue(1);
            }
        }
        else
        {
            assert false;
        }

        return result;
    }

    public IIntValue evaluateKindof(IValue value, Type kindofType)
    {
        assert ((ssc != null) && (ssi != null) && (value != null) && (kindofType != null));

        int result = (value.getTypeId() == kindofType.getTypeId()) ? 1 : 0;

        return vf.newIntValue(result);
    }

    public IValue evaluateLockTestOp(
        int threadId,
        LockTestOp locktestop,
        IValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        ILockValue lockValue = null;

        if (value instanceof ILockValue)
        {
            lockValue = (ILockValue) value;
        }
        else if (value instanceof INullValue)
        {
            throw new NullPointerBogorException();
        }
        else
        {
            assert false;
        }

        int result = 0;

        switch (locktestop)
        {
            case LOCK_AVAILABLE:
                result = lockValue.testLockAvailable(threadId) ? 1 : 0;

                break;

            case WAS_NOTIFIED:
                result = lockValue.testWasNotified(threadId) ? 1 : 0;

                break;

            case HAS_LOCK:
                result = lockValue.testHasLock(threadId) ? 1 : 0;

                break;

            default:
                assert false;
        }

        if (readValues != null)
        {
            readValues.add(value);
        }

        return vf.newIntValue(result);
    }

    public IArrayValue evaluateNewArray(ArrayType arrayType, IValue[] lengths)
    {
        assert ((ssc != null) && (ssi != null) && (arrayType != null) && (lengths != null));

        int size = lengths.length;
        int[] valLengths = new int[size];

        for (int i = 0; i < size; i++)
        {
            assert (lengths[i] instanceof IIntValue);
            valLengths[i] = ((IIntValue) lengths[i]).getInteger();
        }

        return vf.newArrayValue(arrayType, arrayFieldTypes, valLengths);
    }

    public ILockValue evaluateNewLock()
    {
        assert ((ssc != null) && (ssi != null));

        return vf.newLockValue();
    }

    public IRecordValue evaluateNewRecord(RecordType recordType)
    {
        assert ((ssc != null) && (ssi != null) && (recordType != null));

        return vf.newRecordValue(recordType);
    }

    public IValue evaluateUnaryOp(UnaryOp unop, IValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        if (value instanceof IIntValue)
        {
            return ee.evaluateUnaryOp(unop, (IIntValue) value);
        }
        else if (value instanceof ILongValue)
        {
            return ee.evaluateUnaryOp(unop, (ILongValue) value);
        }
        else if (value instanceof IFloatValue)
        {
            return ee.evaluateUnaryOp(unop, (IFloatValue) value);
        }
        else if (value instanceof IDoubleValue)
        {
            return ee.evaluateUnaryOp(unop, (IDoubleValue) value);
        }
        else
        {
            assert false;

            return null;
        }
    }

    public IIntValue evaluateUnaryOp(UnaryOp unop, IIntValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        int result = 0;
        int val = value.getInteger();

        switch (unop)
        {
            case NEG:
                result = -val;

                break;

            case NOT:
                return vf.newIntValue(booleanType, (val == 0) ? 1 : 0);

            case POS:
                result = +val;

                break;

            default:
                assert false;
        }

        return vf.newIntValue(result);
    }

    public ILongValue evaluateUnaryOp(UnaryOp unop, ILongValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        long result = 0;
        long val = value.getLong();

        switch (unop)
        {
            case NEG:
                result = -val;

                break;

            case POS:
                result = +val;

                break;

            default:
                assert false;
        }

        return vf.newLongValue(result);
    }

    public IFloatValue evaluateUnaryOp(UnaryOp unop, IFloatValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        float result = 0;
        float val = value.getFloat();

        switch (unop)
        {
            case NEG:
                result = -val;

                break;

            case POS:
                result = +val;

                break;

            default:
                assert false;
        }

        return vf.newFloatValue(result);
    }

    public IDoubleValue evaluateUnaryOp(UnaryOp unop, IDoubleValue value)
    {
        assert ((ssc != null) && (ssi != null) && (value != null));

        double result = 0;
        double val = value.getDouble();

        switch (unop)
        {
            case NEG:
                result = -val;

                break;

            case POS:
                result = +val;

                break;

            default:
                assert false;
        }

        return vf.newDoubleValue(result);
    }

    public Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo> unsetSchedulingStrategyContextInfo()
    {
        Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo> result = new Pair<ISchedulingStrategyContext, ISchedulingStrategyInfo>(
            this.ssc,
            this.ssi);

        this.ssc = null;
        this.ssi = null;

        return result;
    }

    protected FSMSymbolTable getFSMSymbolTable()
    {
        IState s = ssc.getState();
        int locDesc = s.getLocation(ssc.getThreadId());
        FSMSymbolTable fsmSymbolTable = symbolTable.getFSMSymbolTable(locDesc);

        assert (fsmSymbolTable != null);

        return fsmSymbolTable;
    }

    protected IValue checkRange(Type type, IValue value)
    {
        if (type instanceof IntRangeType)
        {
            IntRangeType irt = (IntRangeType) type;

            if (irt.getWrap())
            {
                int val = ((IIntValue) value).getInteger();
                int lowLimit = irt.getLowLimit();
                int highLimit = irt.getHighLimit();
                int range = highLimit - lowLimit + 1;

                while ((val < lowLimit) || (val > highLimit))
                {
                    if (val < lowLimit)
                    {
                        val += range;
                    }
                    else
                    {
                        val -= range;
                    }
                }

                return vf.newIntValue(val);
            }
            else
            {
                IntRangeType rangeType = (IntRangeType) type;
                int i = ((IIntValue) value).getInteger();

                if ((i > rangeType.getHighLimit())
                    || (i < rangeType.getLowLimit()))
                {
                    throw new RangeBogorException();
                }
            }
        }
        else if (type instanceof LongRangeType)
        {
            LongRangeType lrt = (LongRangeType) type;

            if (lrt.getWrap())
            {
                long val = ((ILongValue) value).getLong();
                long lowLimit = lrt.getLowLimit();
                long highLimit = lrt.getHighLimit();
                long range = highLimit - lowLimit + 1;

                while ((val < lowLimit) || (val > highLimit))
                {
                    if (val < lowLimit)
                    {
                        val += range;
                    }
                    else
                    {
                        val -= range;
                    }
                }

                return vf.newLongValue(val);
            }
            else
            {
                LongRangeType rangeType = (LongRangeType) type;
                long i = ((ILongValue) value).getLong();

                if ((i > rangeType.getHighLimit())
                    || (i < rangeType.getLowLimit()))
                {
                    throw new RangeBogorException();
                }
            }
        }

        return value;
    }

    protected IValue convert(Object o)
    {
        if (o instanceof Integer)
        {
            return vf.newIntValue(((Integer) o).intValue());
        }
        else if (o instanceof Boolean)
        {
            return vf.newIntValue(
                symbolTable.getTypeFactory().getBooleanType(),
                ((Boolean) o).booleanValue() ? 1 : 0);
        }
        else if (o instanceof Long)
        {
            return vf.newLongValue(((Long) o).longValue());
        }
        else if (o instanceof Float)
        {
            return vf.newFloatValue(((Float) o).floatValue());
        }
        else if (o instanceof Double)
        {
            return vf.newDoubleValue(((Double) o).doubleValue());
        }
        else if (o instanceof String)
        {
            return vf.newStringValue((String) o);
        }
        else if (o != null && o.getClass().equals(Object.class))
        {
            return vf.newNullValue();
        }
        else
        {
            assert false;

            return null;
        }
    }

    protected IValue evaluate(Exp exp)
    {
        try
        {
            IValue result = null;

            if (exp instanceof ApplyExp)
            {
                result = evaluateApplyExp((ApplyExp) exp);
            }
            else if (exp instanceof ArrayAccessExp)
            {
                result = evaluateArrayAccessExp((ArrayAccessExp) exp);
            }
            else if (exp instanceof BinaryExp)
            {
                result = evaluateBinaryExp((BinaryExp) exp);
            }
            else if (exp instanceof CastExp)
            {
                result = evaluateCastExp((CastExp) exp);
            }
            else if (exp instanceof ConditionalExp)
            {
                result = evaluateConditionalExp((ConditionalExp) exp);
            }
            else if (exp instanceof ExtExp)
            {
                result = evaluateExtExp((ExtExp) exp);
            }
            else if (exp instanceof FieldAccessExp)
            {
                result = evaluateFieldAccessExp((FieldAccessExp) exp);
            }
            else if (exp instanceof IdExp)
            {
                result = evaluateIdExp((IdExp) exp);
            }
            else if (exp instanceof InstanceofExp)
            {
                result = evaluateInstanceofExp((InstanceofExp) exp);
            }
            else if (exp instanceof KindofExp)
            {
                result = evaluateKindofExp((KindofExp) exp);
            }
            else if (exp instanceof LetExp)
            {
                result = evaluateLetExp((LetExp) exp);
            }
            else if (exp instanceof LiteralExp)
            {
                result = evaluateLiteralExp((LiteralExp) exp);
            }
            else if (exp instanceof LockTestExp)
            {
                result = evaluateLockTestExp((LockTestExp) exp);
            }
            else if (exp instanceof NewArrayExp)
            {
                result = evaluateNewArrayExp((NewArrayExp) exp);
            }
            else if (exp instanceof NewLockExp)
            {
                result = evaluateNewLock();
            }
            else if (exp instanceof NewRecordExp)
            {
                result = evaluateNewRecordExp((NewRecordExp) exp);
            }
            else if (exp instanceof ParenExp)
            {
                result = evaluate(((ParenExp) exp).getExp());
            }
            else if (exp instanceof ThreadTestExp)
            {
                result = evaluateThreadTestExp((ThreadTestExp) exp);
            }
            else if (exp instanceof UnaryExp)
            {
                result = evaluateUnaryExp((UnaryExp) exp);
            }
            else
            {
                assert false;
            }

            assert result != null;

            return result;
        }
        catch (BogorException mce)
        {
            mce.setNode(exp);
            throw mce;
        }
    }

    protected IValue evaluateApplyExp(ApplyExp e)
    {
        String id = e.getId();
        int size = e.getArgCount();
        IValue[] args = new IValue[size];

        for (int i = 0; i < size; i++)
        {
            args[i] = evaluate(e.getArg(i));
        }

        return ee.evaluateApply(id, args);
    }

    /**
     * @throws NullPointerBogorException
     *             if the evaluation of the array-to-be-accessed expression in
     *             <tt>e</tt> is a BIR <tt>null</tt> value
     * @throws IndexOutOfBoundsBogorException
     *             if <tt>arrayValue</tt> is not at least
     *             <tt>indexValue + 1</tt> elements long or
     *             <tt>indexValue < 0</tt>
     */
    protected IValue evaluateArrayAccessExp(ArrayAccessExp e)
    {
        IValue expVal = evaluate(e.getExp());

        if (expVal instanceof INullValue)
        {
            throw new NullPointerBogorException();
        }
        else
        {
            IValue indexVal = evaluate(e.getIndex());

            return ee.evaluateArrayAccess(
                (IArrayValue) expVal,
                (IIntValue) indexVal);
        }
    }

    protected IValue evaluateBinaryExp(BinaryExp e)
    {
        IValue result = null;
        BinaryOp binop = e.getBinaryOp();
        IValue expVal1 = evaluate(e.getExp1());

        if (binop == AND)
        {
            assert (expVal1 instanceof IIntValue);

            int iExpVal1 = ((IIntValue) expVal1).getInteger();

            if (iExpVal1 == 0)
            {
                return expVal1;
            }
        }
        else if (binop == OR)
        {
            assert (expVal1 instanceof IIntValue);

            int iExpVal1 = ((IIntValue) expVal1).getInteger();

            if (iExpVal1 == 1)
            {
                return expVal1;
            }
        }
        else if (binop == IMPLIES)
        {
            assert (expVal1 instanceof IIntValue);

            int iExpVal1 = ((IIntValue) expVal1).getInteger();

            if (iExpVal1 == 0)
            {
                return vf.newIntValue(symbolTable
                    .getTypeFactory()
                    .getBooleanType(), 1);
            }
        }

        IValue expVal2 = evaluate(e.getExp2());
        result = ee.evaluateBinaryOp(binop, expVal1, expVal2);

        return result;
    }

    protected IValue evaluateCastExp(CastExp e)
    {
        // TODO: check why valueType is null
        // Type castType = (Type) symbolTable.getASTTypeTypeTable()
        // .get(e.getType());
        // Type valueType = (Type) getFSMSymbolTable()
        // .getExpTable()
        // .get(e.getExp());
        Type castType = (Type) e.getProperty(Exp.TYPE);
        Type valueType = (Type) e.getExp().getProperty(Exp.TYPE);

        return ee.evaluateCast(castType, valueType, evaluate(e.getExp()));
    }

    protected IValue evaluateConditionalExp(ConditionalExp e)
    {
        IValue condVal = evaluate(e.getCondition());
        assert condVal instanceof IIntValue;

        boolean cond = (((IIntValue) condVal).getInteger() == 0) ? false : true;

        if (cond)
        {
            return evaluate(e.getExp1());
        }
        else
        {
            return evaluate(e.getExp2());
        }
    }

    protected IValue evaluateExtExp(ExtExp e)
    {
        int size = e.getArgCount();
        IValue[] args = new IValue[size];

        StringBuffer sb = new StringBuffer(e.getExtId());
        sb.append(".");
        sb.append(e.getId());

        String expExtId = sb.toString();

        ExpExtension expExt = (ExpExtension) symbolTable
            .getExpActionExtDefTable()
            .get(expExtId);
        int paramCount = expExt.getParameterCount();

        for (int i = 0; i < size; i++)
        {
            if (i >= paramCount)
            {
                if (expExt.getParameterLazyModifier(paramCount - 1))
                {
                    args[i] = vf.newExpASTValue(e.getArg(i));
                }
                else
                {
                    args[i] = evaluate(e.getArg(i));
                }
            }
            else
            {
                if (expExt.getParameterLazyModifier(i))
                {
                    args[i] = vf.newExpASTValue(e.getArg(i));
                }
                else
                {
                    args[i] = evaluate(e.getArg(i));
                }
            }
        }

        return ee.evaluateExt(expExtId, e, (Type[]) e
            .getProperty(ExtExp.TYPE_VAR_ARGS_KEY), args);
    }

    protected IValue evaluateFieldAccessExp(FieldAccessExp e)
    {
        IValue result = null;

        if (e.isConstant())
        {
            Object o = e.getProperty(FieldAccessExp.CONSTANT_KEY);
            result = convert(o);
        }
        else
        {
            IValue expVal = evaluate(e.getExp());

            if (expVal instanceof INullValue)
            {
                throw new NullPointerBogorException();
            }
            else
            {
                if (e.isLength())
                {
                    assert (expVal instanceof IArrayValue);
                    result = vf.newIntValue(((IArrayValue) expVal).getLength());
                }
                else
                {
                    assert (expVal instanceof IRecordValue);

                    Type t = expVal.getType();
                    int index = (t instanceof RecordType) ? ((RecordType) t)
                        .getFieldIndex(e.getId()) : symbolTable
                        .getArrayFieldIndex(e.getId());

                    result = ee.evaluateFieldAccess(
                        (IRecordValue) expVal,
                        index);
                }
            }
        }

        return result;
    }

    protected IValue evaluateIdExp(IdExp e)
    {
        IValue result;
        int index = e.getIndex();
        IState s = ssc.getState();

        if (e.isGlobal())
        {
            if (readGlobals != null)
            {
                readGlobals.add(index);
            }

            result = s.getGlobalValue(index);
        }
        else if (e.isLocal())
        {
            result = s.getLocalValue(ssc.getThreadId(), index);
        }
        else if (e.isFun())
        {
            result = vf.newStringValue(e.getId());
        }
        else
        {
            result = (IValue) bindingMap.get(e.getId());
        }

        return result;
    }

    protected IValue evaluateInstanceofExp(InstanceofExp e)
    {
        Type type = (Type) symbolTable.getASTTypeTypeTable().get(e.getType());

        return ee.evaluateInstanceof(evaluate(e.getExp()), type);
    }

    protected IValue evaluateKindofExp(KindofExp e)
    {
        Type castType = (Type) symbolTable.getASTTypeTypeTable().get(
            e.getType());

        return ee.evaluateKindof(evaluate(e.getExp()), castType);
    }

    protected IValue evaluateLetExp(LetExp e)
    {
        HashMap<String, IValue> oldBindings = new HashMap<String, IValue>();

        int size = e.getBindingCount();
        HashSet<String> addedBindingIds = new HashSet<String>();

        for (int i = 0; i < size; i++)
        {
            String id = e.getBindingId(i);
            IValue arg = evaluate(e.getBindingExp(i));
            IValue o = bindingMap.get(id);

            if (o != null)
            {
                oldBindings.put(id, o);
            }

            bindingMap.put(id, arg);
            addedBindingIds.add(id);
        }

        try
        {
            return evaluate(e.getExp());
        }
        finally
        {
            for (String id : addedBindingIds)
            {
                bindingMap.remove(id);
            }

            bindingMap.putAll(oldBindings);
            addedBindingIds.clear();
            oldBindings.clear();
        }
    }

    protected IValue evaluateLiteral(Literal l)
    {
        IValue result = null;

        if (l instanceof BooleanLiteral)
        {
            result = vf.newIntValue(booleanType, ((BooleanLiteral) l).getBool()
                ? 1
                : 0);
        }
        else if (l instanceof IntLiteral)
        {
            result = vf.newIntValue(((IntLiteral) l).getInteger().intValue());
        }
        else if (l instanceof LongLiteral)
        {
            result = vf.newLongValue(((LongLiteral) l).getLong().longValue());
        }
        else if (l instanceof FloatLiteral)
        {
            result = vf.newFloatValue(((FloatLiteral) l).getFloat());
        }
        else if (l instanceof DoubleLiteral)
        {
            result = vf.newDoubleValue(((DoubleLiteral) l).getDouble());
        }
        else if (l instanceof StringLiteral)
        {
            result = vf.newStringValue(((StringLiteral) l).getString());
        }
        else if (l instanceof NullLiteral)
        {
            result = vf.newNullValue();
        }
        else
        {
            assert false;
        }

        return result;
    }

    protected IValue evaluateLiteralExp(LiteralExp e)
    {
        return evaluateLiteral(e.getLiteral());
    }

    protected IValue evaluateLockTestExp(LockTestExp e)
    {
        IValue expVal = evaluate(e.getExp());

        return ee.evaluateLockTestOp(
            ssc.getThreadId(),
            e.getLockTestOp(),
            expVal);
    }

    protected IValue evaluateNewArrayExp(NewArrayExp e)
    {
        int size = e.getLengthCount();
        IValue[] lengths = new IValue[size];

        for (int i = 0; i < size; i++)
        {
            lengths[i] = evaluate(e.getLength(i));
        }

        return ee
            .evaluateNewArray((ArrayType) e.getProperty(Exp.TYPE), lengths);
    }

    protected IValue evaluateNewRecordExp(NewRecordExp e)
    {
        return ee.evaluateNewRecord((RecordType) symbolTable
            .getASTTypeTypeTable()
            .get(e.getType()));
    }

    protected IValue evaluateThreadTestExp(ThreadTestExp e)
    {
        IState s = ssc.getState();
        IValue expVal = evaluate(e.getExp());
        int tid = ((IIntValue) expVal).getInteger();
        int[] tids = s.getThreadIds();

        if (Util.search(tids, tid) == -1)
        {
            return vf.newIntValue(1);
        }
        else
        {
            return vf.newIntValue(0);
        }
    }

    protected IValue evaluateUnaryExp(UnaryExp e)
    {
        IValue expVal = evaluate(e.getExp());

        return ee.evaluateUnaryOp(e.getUnaryOp(), expVal);
    }

    public Collection<Triple<String, Boolean, OptionScope>> getOptionIds()
    {
        // no supported options
        return new ArrayList<Triple<String, Boolean, OptionScope>>(0);
    }

    public Pair<Domain, Boolean> getOptionDomain(String id)
    {
        // no supported options
        return null;
    }

    public Collection<String> getSuggestedValues(
        String id,
        IBogorConfiguration bc,
        SymbolTable st)
    {
        // no supported options
        return new ArrayList<String>(0);
    }

    public boolean validate(
        String id,
        String value,
        IBogorConfiguration bc,
        SymbolTable st,
        Collection<FileMessage> errors)
    {
        // no supported options
        return false;
    }
}
